Software product development is very much driven by two objectives: short time-to-market and low development costs. However, the current best practice of software development is still expensive, time consuming, and creates unnecessary expenses which often occur in later stages of product development or even after product deployment.
One of the reasons are errors or flaws in the software's source code, such as software bugs, which are both expensive and time consuming to detect. Finding such software bugs, or in turn giving an insurance of their absence, is therefore of great importance in software development.
Research [AS] done by the consulting firm @stake Inc. (now acquired by Symantec) shows that resolving for example, security related bugs is about twice as expensive during the testing phase than during the implementation phase, and it is even about ten times more expensive after deployment. This does not include indirect costs such as loss of customer goodwill or the occurrence of liabilities.
Dynamic testing is one approach to program analysis. Given a set of input values the software to be tested is executed and its behaviour observed. In particular, the output, (i.e., the result of executing the program) is compared to what has been specified. Dynamic testing is mostly concerned about the functional correctness of code. It provides answers to questions like: “Does this program compute the square root of the input value?” or “Does this program return the list of employees in alphabetical order?” Typically, testing is not exhaustive. This means, there is no way to test for every possible scenario. Moreover, it is cumbersome to generate appropriate test cases and time consuming to run those tests.
Static analysis, as the name suggests, is a static approach to program analysis. This can be done at compile-time or even before, when only certain code fragments are available. Static analysis can be described as a sophisticated way of “looking” at the code, examining it, and approximating its behaviour. Just by observing the code structure in a smart way many properties can be checked (e.g., “Are all declared variables initialised before the program reaches the point of their first use?”, “Are programming guidelines respected?”, or “Are certain programming constructs such as pointers handled in a safe manner?”).
The class of problems addressed by static analysis is usually different to the ones addressed by dynamic testing. However, many static properties have an immediate impact for dynamic properties. For instance, a pointer mishandling can lead to a program crash which certainly violates functional requirements. Moreover, static analysis is typically exhaustive (i.e., if no property violation (bug) is found, it is guaranteed that this bug will not occur).
It has been shown in theory that static analysis problems can be stated as model checking problems [SS98]. Model checking is a technique that allows the searching of large finite state spaces in a very efficient manner with respect to certain properties. Typically, the state space is represented as a transition system (i.e., a graph annotated with labels) and the properties are expressed in temporal logic formulas over these labels. Transforming a static analysis problem into a model checking problem has two advantages. Firstly, there are free tools available that solve model checking problems efficiently and secondly, many static analysis properties can be expressed in a natural way as temporal logic formulae.
Consider the labelled (annotated) control flow graph (CFG) as depicted in FIG. 11. The CFG represents the (control) structure of a program, and contains information about the location of loops, branches, or straight line code. It typically does not contain “deeper” information (e.g., where variable i is declared or where it is used). The annotations do that, for example, they are labels added to every location where i is declared or used.
A static analysis/model checking property can be: “It is always the case that if variable i is declared it must be used somewhere in the future.” This property is already natural language expression of temporal logic and looks in a more formal notation as follows:AG(i_declaredEF i_used)where AG means (informally) “always” and EF “somewhere in the future”. The labels i_declared and i_used are attached to those program locations where they are true. Given such a CFG (which is a transition system) annotated with labels, model checking can check formulas as the above automatically.
Any discussion of documents, acts, materials, devices, articles or the like which has been included in the present specification is solely for the purpose of providing a context for the present invention. It is not to be taken as an admission that any or all of these matters form part of the prior art base or were common general knowledge in the field relevant to the present invention as it existed before the priority date of each claim of this application.